nLab lesser limited principle of omniscience

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Definition

The lesser limited principle of omniscience (LLPOLLPO) is a principle of omniscience which states that, if the existential quantification of the conjunction of two decidable propositions is false, then one of their separate existential quantifications is false. That is,

(x,P(x)¬P(x))(y,Q(y)¬Q(y))¬(x,P(x)y,Q(y))¬(x,P(x))¬(y,Q(y)), (\forall x, P(x) \vee \neg{P(x)}) \Rightarrow (\forall y, Q(y) \vee \neg{Q(y)}) \Rightarrow \neg(\exists x, P(x) \wedge \exists y, Q(y)) \Rightarrow \neg(\exists x, P(x)) \vee \neg(\exists y, Q(y)) ,

or equivalently

(x,P(x)¬P(x))(y,Q(y)¬Q(y))¬(x,P(x)y,Q(y))(x,¬P(x))(y,¬Q(y)). (\forall x, P(x) \vee \neg{P(x)}) \Rightarrow (\forall y, Q(y) \vee \neg{Q(y)}) \Rightarrow \neg(\exists x, P(x) \wedge \exists y, Q(y)) \Rightarrow (\forall x, \neg{P(x)}) \vee (\forall y, \neg{Q(y)}) .

If one takes the domains of quantification to be subsingletons, one get de Morgan's law ¬(pq)¬p¬q\neg(p \wedge q) \Rightarrow \neg{p} \vee \neg{q} (DMDM), which is weaker than EMEM; conversely, DMDM implies LLPOLLPO (over any domain). Again, Bishop's LLPOLLPO takes the domain to be \mathbb{N}, giving a principle weaker than DMDM (and also weaker than LPO LPO_{\mathbb{N}}).

Stated set-theoretically, the lesser limited principle of omniscience for AA (LLPO ALLPO_A) states that, given functions f,g:A{0,1}f, g\colon A \to \{0,1\}, if 1imfimg1 \notin \im f \cap \im g, then 1imf1 \notin \im f or 1img1 \notin \im g. So Bishop's LLPOLLPO is LLPO LLPO_{\mathbb{N}}.

In the internal logic

In set theory, there are actually two different notions of logic: there is the external predicate logic used to define the set theory itself, and there is the internal predicate logic induced by the set operations on subsingletons and injections. In particular,

  • An internal proposition is a set PP such that for all elements xAx \in A and yAy \in A, x=yx = y.

  • The internal proposition true is a singleton \top.

  • The internal proposition false is the empty set

  • The internal conjunction of two internal propositions PP and QQ is the cartesian product P×QP \times Q of PP and QQ.

  • The internal disjunction of two internal propositions PP and QQ is the image of the unique function ! PQ:PQ1!_{P \uplus Q}:P \uplus Q \to 1 from the disjoint union of PP and QQ to the singleton \top.

PQ=im(! PQ)P \vee Q = \mathrm{im}(!_{P \uplus Q})
  • The internal implication of two internal propositions PP and QQ is the function set PQP \to Q between PP and QQ.

  • The internal negation of an internal proposition PP is the function set from PP to the empty set

¬P=P\neg P = P \to \emptyset
  • An internal proposition PP is a decidable proposition if it comes with a function χ P:P2\chi_P:P \to 2 from PP to the boolean domain 22.

  • An internal predicate on a set AA is a set PP with injection i:PAi:P \hookrightarrow A, whose family of propositions indexed by xAx \in A is represented by the preimages i *(x)i^*(x).

  • The internal existential quantifier of an internal predicate i:PAi:P \hookrightarrow A is the image of the unique function ! P:P!_P:P \to \top into the singleton \top.

AP=im(! P)\exists_A P = \im(!_P)
AP={fP A|xA,f(x)i *(x)}\forall_A P = \{f \in P^A \vert \forall x \in A, f(x) \in i^*(x) \}
  • An internal predicate i:PAi:P \hookrightarrow A is a decidable proposition if it comes with a function χ P(x):i *(x)2\chi_P(x):i^*(x) \to 2 into the boolean domain for all elements xAx \in A, or equivalently if it comes with a function χ P:A2\chi_P:A \to 2 from AA to the boolean domain 22.

The internal LLPO for a family of sets (A z) zI(A_z)_{z \in I} is the LLPO for each A zA_z stated in the internal logic of the set theory:

  • The internal LPO for a family of sets (A z) zI(A_z)_{z \in I} holds only for the internal predicates i:PA zi:P \hookrightarrow A_z which comes with an internal predicate j:QA zj:Q \hookrightarrow A_z such that i *(x)=¬j *(x)i^*(x) = \neg j^*(x) for all xA zx \in A_z.

In particular, the internal LLPO for the family of all sets in UU is weak excluded middle in UU.

The internal LLPO, like all internal versions of axioms, are weaker than the external version of LLPO, since while bounded separation implies that one can convert any external predicate xAP(x)x \in A \vdash P(x) on a set AA to an internal predicate {xA|P(x)}A\{x \in A \vert P(x)\} \hookrightarrow A, it is generally not possible to convert an internal predicate to an external predicate without a reflection rule which turns subsingletons in the set theory into propositions in the external logic.

Equivalent statements

There are various other results that are equivalent to the principles of omniscience. Here are a few:

  • Let [0,1]/(01)[0,1]/(0 \sim 1) be the quotient of the unit interval that identifies the endpoints, and let /\mathbb{R}/\mathbb{Z} be the quotient ring; both are classically isomorphic to the circle 𝕊 1\mathbb{S}^1. (Constructively, we take 𝕊 1\mathbb{S}^1 to be /\mathbb{R}/\mathbb{Z}, although S 1S^1 can also be constructed as a completion of [0,1]/(01)[0,1]/(0 \sim 1).) Constructively, there is an injection [0,1]/(01)/[0,1]/(0 \sim 1) \hookrightarrow \mathbb{R}/\mathbb{Z}, which is a bijection if and only if the LLPOLLPO holds (for the appropriate kind of real number).

  • The analytic LLPO for the Cauchy real numbers is equivalent to the LLPO for the natural numbers.

There are various other results that are related to the principles of omniscience. Here are a few:

Untruncated LLPO in dependent type theory

In the context of dependent type theory, the lesser limited principles of omniscience can be translated in two ways, by interpreting “or” as propositionally truncated (“merely or”) or untruncated (“purely or”). The relationships between the truncated and untruncated LLPO are as follows are:

Thus, untruncated LLPO is strictly stronger than truncated LLPO, unlike the case for LPO and WLPO.

Models

  • The (analytic) LLPO holds in Johnstone’s topological topos, as a consequence of the preservation of finite closed unions by the inclusion of sequential spaces.

References

Last revised on July 27, 2024 at 16:44:06. See the history of this page for a list of all contributions to it.